COMMENT ⊗   VALID 00016 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub[let,jmc]" source
C00004 00003	.GROUP SKIP 20
C00005 00004	#. %3Introduction - The Qualification Problem%1
C00011 00005	.<<#. %3The Need for Non-Monotonic Reasoning%1>>
C00016 00006	.<<#. %3Missionaries and Cannibals%1>>
C00031 00007	.<<#. %3The Formalism of Circumscription%1>>
C00040 00008	.<<#. %3Domain Circumscription%1>>
C00044 00009	.<<semantics>>
C00048 00010	.<<more on blocks>>
C00054 00011	.<<.bb Circumscription in the Blocks World>>
C00063 00012	.<<#. %3Remarks%1>>
C00071 00013	.<<NOTES ON POSSIBLE INCLUSIONS>>
C00084 00014	.<<addendum>>
C00092 00015	.<<#. %3References%1>>
C00096 00016
C00097 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.item←0
.at "qi" ⊂"%8r%*"⊃
.at "qe" ⊂"%8q%*"⊃
.font C "zero30"
.at "Goedel" ⊂"G%C:%*odel"⊃
.at "qx" ⊂"%C¬%*x"⊃
.at "qy" ⊂"%C¬%*y"⊃
.at "qF" ⊂"%AF%*"⊃
.at "qG" ⊂"%AY%*"⊃
.turn on "_" for "#"
.turn on "α"
.turn on "↑[]"
.turn on "→"
.GROUP SKIP 20
.cb CIRCUMSCRIPTION - A FORM OF NON-MONOTONIC REASONING

.cb by John McCarthy

.cb Stanford University


Abstract: Humans and intelligent computer programs must often jump to
the conclusion that the objects they can determine to have certain
properties or relations are the only objects that do.
%2Circumscription%1 formalizes such
conjectural reasoning.

.skip to column 1
#. %3Introduction - The Qualification Problem%1

	(McCarthy 1960) proposed a program with "common sense"
that would represent what it knows (mainly) by sentences
in a suitable logical language.  It would decide what to do by
deducing a conclusion that it should perform a certain act.
Performing the act would create a new situation, and it
would again decide what to do.  This requires
representing both knowledge about the particular situation
and general common sense knowledge as sentences of logic.

	The "qualification problem",
immediately arose in representing
general common sense knowledge.  It seemed that in order to
fully represent the conditions for the successful performance of
an action, an impractical and implausible number of qualifications
would have to be included in the sentences expressing them.
For example, the successful use of a boat to cross
a river requires, if the boat is a rowboat, that the oars
and rowlocks be present and unbroken, and that they fit each other.
Many other qualifications can be added, making the rules
for using a rowboat almost impossible to apply, and yet anyone
will still be able to think of additional requirements not
yet stated.

	Circumscription is a rule of conjecture that can be
used by a person or program for "jumping to
certain conclusions".  Namely,
%2the objects that can be shown to have
a certain property P by reasoning from certain
facts A are all the objects that satisfy P%1.
More generally, circumscription can be used to conjecture that
the tuples %2<x,y_..._,z>%1 that can be shown to satisfy a
relation %2P(x,y,_..._,z)%1 are all the tuples satisfying this relation.
Thus we ⊗circumscribe the set of relevant tuples.

	We can postulate that a boat can be used to cross
a river unless "something" prevents it.
Then circumscription may be used to conjecture that the
only entities that can prevent the use of the boat are
those whose existence follows from the facts at hand.
If no lack of oars or other circumstance preventing boat use is deducible,
then the boat is concluded to be usable.
The correctness of this conclusion depends on our having
"taken into account" all relevant facts when we made the circumscription.

	Circumscription formalizes several processes of human informal reasoning.
For example, common sense reasoning is ordinarily ready to jump to the
conclusion that a tool can be used for its intended purpose unless
something prevents its use.  Considered purely extensionally, such
a statement conveys no information; it seems merely to assert that
a tool can be used for its intended purpose unless it can't.
Heuristically, the statement is not just a
tautologous disjunction; it suggests forming a plan to use the tool.

	Even when a program does not reach its conclusions by manipulating
sentences in a formal language, we can often profitably analyze its
behavior by considering it to %2believe%1 certain sentences when it is
in certain states, and we can study how these %2ascribed beliefs%1 change
with time.  See (McCarthy 1979a).  When we do such analyses,
we again discover that successful people and programs must jump to such
conclusions.


.<<#. %3The Need for Non-Monotonic Reasoning%1>>
.skip 2
#. %3The Need for Non-Monotonic Reasoning%1

	We cannot get circumscriptive reasoning capability by
adding sentences to an axiomatization or by adding an ordinary
rule of inference to mathematical logic.  This is because
the well known systems of mathematical logic have the
following %2monotonicity property%1.  If a sentence ⊗q follows
from a collection ⊗A of sentences and %2A_⊂_B%1, then ⊗q follows
from ⊗B.  In the notation of proof theory: if %2A_qi_q%1 and
%2A_⊂_B%1, then %2B_qi_q%1.
Indeed a proof from the premisses ⊗A is a
sequence of sentences each of which is a either a premiss, an axiom or
follows from a subset of the sentences occurring earlier in the
proof by one of the rules of inference.  Therefore, a proof from ⊗A can also
serve as a proof from ⊗B. 
The semantic notion of entailment is also monotonic; we say that
⊗A entails ⊗q (written %2A_qe_q%1)
if ⊗q is true in all models of ⊗A.  But if %2A_qe_q%1 and
%2A_⊂_B%1, then every model of ⊗B is also a model of
⊗A, which shows that %2B_qe_q%1.

	%2Circumscription%1 is a formalized %2rule of conjecture%1 that
can be used along with the %2rules of inference%1 of first order logic.
%2Predicate circumscription%1 assumes that entities satisfy a given
predicate only if they have to on the basis of a collection of facts.
%2Domain circumscription%1 conjectures that the "known" entities are all
there are.  It turns out that domain circumscription, previously called
%2minimal inference%1, can be subsumed under predicate circumscription.

	We will argue using examples that humans use such "non-monotonic"
reasoning and that it is required for intelligent behavior.  The default
case reasoning of many computer programs (Reiter 1980) and the use of
THNOT in MICROPLANNER (Sussman, et. al.  1971) programs are also examples
of non-monotonic reasoning, but possibly of a different kind from those
discussed in this paper.  (Hewitt 1972) gives the basic ideas of the
PLANNER approach.

	The result of applying circumscription to a
collection ⊗A of facts is a sentence schema that
asserts that the only tuples satisfying a predicate ⊗P(x,_..._,z) are
those whose doing so follows from the sentences of ⊗A. 
Since adding more sentences to ⊗A might make ⊗P applicable to more
tuples, circumscription is not monotonic.
Conclusions derived from circumscription are conjectures
that ⊗A includes all the relevant
facts and that the objects whose existence follows from ⊗A are
all the relevant objects.

	A heuristic program might use circumscription in various
ways.  Suppose it circumscribes some facts and
makes a plan on the basis of the conclusions reached.  It might
immediately carry out the plan, or be more cautious and look for
additional facts that might require modifying it.

	Before introducing the formalism, we informally discuss a well known
problem whose solution seems to
involve such non-monotonic reasoning.
.<<#. %3Missionaries and Cannibals%1>>
.skip 2
#. %3Missionaries and Cannibals%1

	The %2Missionaries and Cannibals%1 puzzle, much used in AI,
contains more than enough detail to illustrate many of the issues.

	%2"Three missionaries and three cannibals come to a river.  A
rowboat that seats two is available.  If the cannibals ever
outnumber the missionaries on either bank of the river, the
missionaries will be eaten.  How shall they cross the river?"%1.

	Obviously the puzzler is expected to devise a strategy of rowing
the boat back and forth that gets them all across and avoids the disaster.

	Amarel (1971) considered several representations of the problem
and discussed criteria whereby the following representation is preferred
for purposes of AI, because it leads to the smallest state space that must
be explored to find the solution.  A state is a triple
comprising the numbers of missionaries, cannibals and boats on the starting
bank of the river.  The initial state is 331,
the desired final state is 000, and one solution is given by the
sequence (331,220,321,300,311,110,221,020,031,010,021,000).

	We are not presently concerned with the heuristics of the problem
but rather with the correctness of the reasoning that goes from the
English statement of the problem to Amarel's state space representation.
A generally intelligent computer program should be able to
carry out this reasoning.  Of
course, there are the well known difficulties in making computers
understand English, but suppose the English sentences describing the
problem have already been rather directly translated into first order
logic.  The correctness of Amarel's representation is not an ordinary
logical consequence of these sentences for two further reasons.
.if false then begin
CAN WE EVEN STATE THE CORRECTNESS OF AMAREL'S REPRESENTATION?
.end

	First, nothing has been stated about the properties of boats or
even the fact that rowing across the river doesn't change the numbers of
missionaries or cannibals or the capacity of the boat.  Indeed it hasn't
been stated that situations change as a result of action.  These facts follow
from common sense knowledge, so let us imagine that common sense
knowledge, or at least the relevant part of it, is also expressed in first
order logic.

	The second reason we can't ⊗deduce the propriety of Amarel's
representation is deeper.  Imagine giving someone the problem, and after
he puzzles for a while, he suggests going upstream half a mile and
crossing on a bridge.  "What bridge", you say.  "No bridge is mentioned in
the statement of the problem."  And this dunce replies, "Well, they don't
say there isn't a bridge".  You look at the English and even at
the translation of the English into first order logic, and you must admit
that "they don't say" there is no bridge.  So you modify the problem
to exclude bridges
and pose it again, and the dunce proposes a helicopter, and after you
exclude that, he proposes a winged horse or that the others hang onto the
outside of the boat while two row.

	You now see that while a dunce, he is
an inventive dunce.  Despairing of getting him to accept the problem
in the proper puzzler's spirit, you tell him the solution.  To your further
annoyance, he attacks your solution on the grounds that the boat might
have a leak or lack
oars.  After you rectify that omission from the statement
of the problem, he suggests that a sea
monster may swim up the river and may swallow the boat.  Again you are
frustrated, and you look for a mode of reasoning that will settle his hash
once and for all.

	In spite of our irritation with the dunce, it would be
cheating to put into the statement of the problem
that there is no other way to cross the river
than using the boat and that nothing can go wrong with the boat.
A human doesn't need such an ad hoc narrowing of the problem, and indeed
the only watertight way to do it might amount to specifying the Amarel
representation in English.  Rather we want to avoid the excessive
qualification and get the Amarel representation by common sense reasoning
as humans ordinarily do.

	Circumscription is one candidate for accomplishing this.
It will allow us to conjecture that no relevant objects exist in certain
categories except those
whose existence follows from the statement of the problem and common
sense knowledge.
When we ⊗circumscribe the first order logic statement of the problem together
with the common sense facts about boats etc., we will
be able to conclude that there is
no bridge or helicopter.  "Aha", you say, "but there won't be any oars
either".  No, we get out of that as follows:  It is a part of common
knowledge that a boat can be used to cross a river %2unless there is
something wrong with it or something else prevents using it%1, and if our
facts don't require that there be something that prevents crossing the river,
circumscription will generate the conjecture that there isn't.
The price is introducing as entities in our language the "somethings" that
may prevent the use of the boat.

	If the statement of the problem were extended to mention a bridge,
then the circumscription of the problem statement would no longer permit
showing the non-existence of a bridge, i.e. a conclusion that can be drawn
from a smaller collection of facts can no longer be drawn from a larger.
This non-monotonic character of circumscription is just what we want for
this kind of problem.  The statement, %2"There is a bridge a mile
upstream, and the boat has a leak."%1
doesn't contradict the text of the problem, but its addition
invalidates the Amarel representation.

	In the usual sort of puzzle, there is a convention that there are
no additional objects beyond those mentioned in the puzzle or whose
existence is deducible from the puzzle and common sense knowledge.
The convention can be explicated as applying circumscription
to the puzzle statement and a certain part of common sense knowledge.
However,
if one really were sitting by a river bank and these six people came
by and posed their problem, one wouldn't take the circumscription
for granted, but one ⊗would consider the result of circumscription as a
hypothesis.  In puzzles, circumscription seems to be a rule of inference,
while in life it is a rule of conjecture.

.if false then begin
	At first I considered this solution ad hoc,
but I am now convinced that it is a correct explication of the use of
%2normality%1; i.e. unless something abnormal exists, an object can
be used to carry out its normal function.
.end

	Some have suggested that the difficulties might be avoided by
introducing probabilities.  They suggest that the existence of a bridge is
improbable.  The whole situation involving cannibals with the
postulated properties cannot be regarded as having a probability, so it
is hard to take seriously
the conditional probability of a bridge given the hypotheses.  More to the point,
we mentally propose to ourselves the normal non-bridge non-sea-monster
interpretation ⊗before considering these extraneous possibilities, let
alone their probabilities, i.e. we usually don't even introduce the sample
space in which these possibilities are assigned whatever probabilities one
might consider them to have.  Therefore, regardless of our knowledge of
probabilities, we need a way of formulating the normal situation from the
statement of the facts, and non-monotonic reasoning seems to be required.
The same considerations seem to apply to fuzzy logic.

	Using circumscription requires that common sense knowledge
be expressed
in a form that says a boat can be used to cross rivers unless there is
something that prevents its use.  In particular, it looks like we must introduce
into
our ⊗ontology (the things that exist) a category that includes
%2something wrong with a boat%1 or a category that includes
%2something that may prevent its use%1.
Incidentally, once we have decided to admit %2something wrong with the boat%1,
we are inclined to admit a %2lack of oars%1 as such a something and to ask
questions like, %2"Is a lack of oars all that is wrong with the boat?%1".

	Some philosophers
and scientists may be reluctant to introduce such ⊗things, but since
ordinary language allows %2"something wrong with the boat"%1
we shouldn't be hasty in excluding it.  Making a suitable
formalism is likely to be technically difficult as well as
philosophically problematical,
but we must try.

	We challenge anyone who thinks he can avoid such entities to
express in his favorite formalism, %2"Besides leakiness, there is something
else wrong with the boat"%1.  A good solution would avoid counterfactuals
as this one does.

	Circumscription may help understand natural language,
because if the use of natural language involves something like
circumscription, it is understandable that the expression of general
common sense facts in natural language will be difficult without
some form of non-monotonic reasoning.
.<<#. %3The Formalism of Circumscription%1>>
.skip 2
#. %3The Formalism of Circumscription%1

	Let ⊗A be a sentence of first order logic containing a
predicate symbol  %2P(x%41%*,_..._,x%4n%*)%1 which we will write %2P(qx)%1.
We write %2A(qF)%1 for the result of replacing all occurrences of ⊗P in ⊗A by
the predicate expression qF%1.  (As well as predicate symbols, suitable
λ-expressions are allowed as predicate expressions).

%3Definition: The circumscription of ⊗P in ⊗A(P) is the sentence schema%1

!!a1:	%2A(qF) ∧ ∀qx.(qF(qx) ⊃ P(qx)) _⊃_ ∀qx.(P(qx) ⊃ qF(qx))%1.

	({eq a1}) can be regarded as asserting that the only tuples %2(qx)%1
that satisfy ⊗P are those that have to - assuming the sentence ⊗A. 
Namely, ({eq a1}) contains a predicate parameter qF for which
we may subsitute an arbitrary predicate expression.  (If we were
using second order logic, there would be a quantifier ∀qF in front
of ({eq a1})).  Since ({eq a1}) is an implication, we can assume
both conjuncts on the left, and ({eq a1}) lets us
conclude the sentence on the right.
The first conjunct %2A(qF)%1 expresses the assumption
that qF satisfies the conditions
satisfied by ⊗P, and the second %2∀qx.(qF(qx)_⊃_P(qx))%1 expresses
the assumption that the entities satisfying qF are a subset of those
that satisfy ⊗P.  The conclusion asserts the converse of the second
conjunct which tells us that in this case, qF and ⊗P must coincide.

	We write %2A_qi%4P%*_q%1 if the sentence ⊗q can be obtained by
deduction from the result of circumscribing ⊗P in ⊗A.  As we shall
see %2qi%4P%1 is a non-monotonic form of inference, which we shall
call %2circumscriptive inference%1.

	A slight generalization allows circumscribing several predicates
jointly; thus jointly circumscribing ⊗P and ⊗Q in ⊗A(P,Q) leads to

!!a11:	%2A(qF,qG) ∧ ∀qx.(qF(qx) ⊃ P(qx)) ∧ ∀qy.(qG(qy) ⊃ Q(qy)) _⊃_
∀qx.(P(qx) ⊃ qF(qx)) ∧ ∀qy.(Q(qy) ⊃ qG(qy))%1

in which we can simultaneously substitute for qF and qG.
The relation %2A_qi%4P,Q%*_q%1 is defined in a corresponding way.
Although we don't give examples of joint circumscription in this paper,
we believe it will be important in some AI applications.

	Consider the following examples:

	1. In the blocks world, the sentence ⊗A may be

!!a2:	%2isblock A ∧ isblock B ∧ isblock C%1

asserting that ⊗A, ⊗B and ⊗C are blocks.  Circumscribing ⊗isblock in ({eq a2})
gives the schema

!!a3:	%2qF(A) ∧ qF(B) ∧ qF(C) ∧ ∀x.(qF(x) ⊃ isblock x) _⊃_ ∀x.(isblock x ⊃ qF(x))%1.

If we now substitute

!!a4:	%2qF(x) ≡ (x = A ∨ x = B ∨ x = C)%1

into ({eq a3}) and use ({eq a2}), the left side of the implication
is seen to be true, and this gives

!!a5:	%2∀x.(isblock x ⊃ (x = A ∨ x = B ∨ x = C))%1,

which asserts that the only blocks are ⊗A, ⊗B and ⊗C, i.e. just those
objects that ({eq a2}) requires to be blocks.  This example is rather
trivial, because ({eq a2}) provides no way of generating new blocks
from old ones.  However, it shows that circumscriptive inference is
non-monotonic since if we adjoin ⊗isblock_D to ({eq a2}), we will no
longer be able to infer ({eq a5}).

	2. Circumscribing the disjunction

!!a6a:	%2isblock A ∨ isblock B%1

leads to

!!a6b:	%2(qF(A) ∨ qF(B)) ∧ ∀x.(qF(x) ⊃ isblock x) _⊃_ ∀x.(isblock x ⊃ qF(x))%1.

We may then substitute successively %2qF(x) ≡ (x=A)%1 and %2qF(x) ≡ (x=B)%1,
and these give respectively

!!a6c:	%2(A=A ∨ A=B) ∧ ∀x.(x=A ⊃ isblock x) _⊃_ ∀x.(isblock x ⊃ x=A)%1,

which simplifies to

!!a6d:	%2isblock A ⊃ ∀x.(isblock x ⊃ x=A)%1

and

!!a7c:	%2(B=A ∨ B=B) ∧ ∀x.(x=B ⊃ isblock x) _⊃_ ∀x.(isblock x ⊃ x=B)%1,

which simplifies to

!!a6e:	%2isblock B ⊃ ∀x.(isblock x ⊃ x=B)%1.

({eq a6d}), ({eq a6e}) and ({eq a6a}) yield

!!a6f:	%2∀x.(isblock x ⊃ x=A) ∨ ∀x.(isblock x ⊃ x=B)%1,

which asserts that either ⊗A is the only block or ⊗B is the only block.

	3. Consider the following algebraic axioms for natural numbers,
i.e. non-negative integers,
appropriate when
we aren't supposing that natural numbers are the only objects.

!!a6:	%2isnatnum 0 ∧ ∀x.(isnatnum x ⊃ isnatnum succ x)%1.

Circumscribing ⊗isnatnum in ({eq a6}) yields

!!a7:	%2qF(0) ∧ ∀x.(qF(x) ⊃ qF(succ x)) ∧ ∀x.(qF(x) ⊃ isnatnum x)
_⊃_ ∀x.(isnatnum x ⊃ qF(x))%1.

({eq a7}) asserts that the only natural numbers are those objects that ({eq a6})
forces to be natural numbers, and this is essentially the usual axiom schema of
induction.  We can get closer to the usual schema by substituting
%2qF(x)_≡_qG(x)_∧_isnatnum_x%1.  This and ({eq a6}) make
the second conjunct drop out giving

!!a7a:	%2qG(0) ∧ ∀x.(qG(x) ⊃ qG(succ x)) ⊃ ∀x.(isnatnum x ⊃ qG(x))%1.

	4. Returning to the blocks world, suppose we have a predicate
⊗on(x,y,s) asserting that block ⊗x is on block ⊗y in situation ⊗s.  Suppose
we have another predicate ⊗above(x,y,s) which asserts that block
⊗x is above block ⊗y in situation ⊗s.  We may write

!!a8:	%2∀x y s.(on(x,y,s) ⊃ above(x,y,s))%1

and

!!a9:	%2∀x y z s.(above(x,y,s) ∧ above(y,z,s) ⊃ above(x,z,s))%1,

i.e. ⊗above is a transitive relation.  Circumscribing ⊗above in
({eq a8})∧({eq a9}) gives

.begin preface 0

.skip 1
!!a10:	∂(10)%2∀x y s.(on(x,y,s) ⊃ qF(x,y,s))

→∧_∂(10)∀x y z s.(qF(x,y,s) ∧ qF(y,z,s) ⊃ qF(x,z,s))

→∧_∂(10)∀x y s.(qF(x,y,s) ⊃ above(x,y,s))

∂(20)⊃ ∀x y s.(above(x,y,s) ⊃ qF(x,y,s))%1
.end

which tells us that ⊗above is the transitive closure of ⊗on. 

	In the preceding two examples, the schemas produced
by circumscription play the role of
axiom schemas rather than being just conjectures.
.<<#. %3Domain Circumscription%1>>
.skip 2
#. %3Domain Circumscription%1

	The form of circumscription described in this paper generalizes
an earlier version called %2minimal inference%1.  Minimal inference
has a semantic counterpart called %2minimal entailment%1, and both are
discussed in (McCarthy 1977) and more extensively in (Davis 1980).
The general idea of minimal entailment is that a sentence ⊗q is minimally
entailed by an axiom ⊗A, written %2A_qe%4m%*_q%1, if ⊗q is true in all
%2minimal models%1 of ⊗A, where one model if is considered less than another
if they agree on common elements, but the domain of the larger many contain
elements not in the domain of the smaller.
We shall call the earlier form %2domain circumscription%1 to contrast it
with the %2predicate circumscription%1 discussed in this paper.

	The domain circumscription of the sentence ⊗A is the sentence

!!b1:	%2Axiom(qF) ∧ A↑[qF] ⊃ ∀x.qF(x)%1,

where %2A↑[qF]%1 is the relativization of ⊗A with respect to qF and
is formed by replacing each universal quantifier ⊗∀x. in ⊗A by 
%2∀x.qF(x)_⊃%1 and each existential quantifier %2∃x.%1 by %2∃x.qF(x)_∧%1.
%2Axiom(qF)%1 is the conjunction of sentences %2qF(a)%1 for each constant
⊗a and sentences %2∀x.(qF(x)_⊃_qF(f(x)))%1 for each function
symbol ⊗f and the corresponding sentences for functions of higher
arities.

	Domain circumscription can be reduced to predicate circumscription
by relativizing ⊗A with respect to a new one place predicate
called (say) ⊗all, then circumscribing ⊗all in %2A↑[all]_∧_Axiom(all)%1,
thus getting

!!b2:	%2Axiom(qF) ∧ A↑[qF] ∧ ∀x.(qF(x) ⊃ all(x)) _⊃_ ∀x.(all(x) ⊃ qF(x))%1.

Now we justify our using the name ⊗all by adding the axiom %2∀x.all(x)%1
so that ({eq b2}) then simplifies precisely to ({eq b1}).

	In the case of the natural numbers, the domain circumscription of
%3true%1, the identically true sentence, again leads to the axiom
schema of induction.  Here ⊗Axiom does all the work, because it
asserts that 0 is in the domain and that the domain is closed under
the successor operation.
.<<semantics>>
.skip 2
#. %3The Model Theory of Predicate Circumscription%1

	This treatment is similar to Davis's (1980) treatment of
domain circumscription.  Pat Hayes (1979) pointed out that
the same ideas would work.

	The intuitive idea of circumscription is saying that a tuple
qx satisfies the predicate ⊗P only if it has to.
It has to satisfy ⊗P if this follows from
the sentence ⊗A.  The model-theoretic counterpart of circumscription
is %2minimal entailment%1.  A sentence ⊗q is minimally entailed
by ⊗A, iff ⊗q is true in all minimal models of ⊗A, where a model
is minimal if as few as possible tuples qx satisfy the
predicate ⊗P.  More formally, this works out as follows.

%3Definition: Let ⊗M(A) and ⊗N(A) be models of the sentence ⊗A. 
We say that ⊗M is a submodel of ⊗N in ⊗P, 
writing %2M_≤%4P%*_N%3, if ⊗M and ⊗N have the same domain,
all other predicate symbols in ⊗A besides ⊗P have the
same extensions in ⊗M and ⊗N, but the extension of ⊗P in ⊗M is
included in its extension in ⊗N. 

%3Definition: A model ⊗M of ⊗A is called minimal in
⊗P iff %2M'_≤%4P%*_M%1 only if %2M'_=_M%1.  As discussed by
Davis (1980), minimal models don't always exist%1.

%3Definition: We say that ⊗A minimally entails ⊗q with respect to
⊗P, written %2A_qe%4P%*_q%3 provided ⊗q is true in all
models of ⊗A that are minimal in ⊗P. 

%3Theorem: Any instance of the circumscription of ⊗P in ⊗A is
true in all models of ⊗A minimal in ⊗P, i.e. is minimally
entailed by ⊗A in %2P%1. 

Proof: Let ⊗M be a model of ⊗A minimal in ⊗P.  Let ⊗P' be a
predicate satisfying the left side of ({eq a1}) when substituted
for qF.  By the second conjunct of the left side ⊗P is an
extension of ⊗P'.  If the right side of ({eq a1}) were not
satisfied, ⊗P would be a proper extension of ⊗P'.  In that case,
we could get a proper submodel ⊗M' of ⊗M by letting ⊗M' agree
with ⊗M on all predicates except ⊗P and agree with ⊗P' on ⊗P.  This
would contradict the assumed minimality of ⊗M. 

%3Corollary: If %2A qi%4P%* q%3, then %2A qe%4P%* q%1.

	While we have discussed minimal entailment in a single
predicate ⊗P, the relation %2<%4P,Q%1, models minimal in ⊗P and ⊗Q, 
and %2qe%4P,Q%1 have corresponding properties and a corresponding
relation to the syntactic notion %2qi%4P,Q%1 mentioned earlier.
.<<more on blocks>>
.skip 2
#. %3More on Blocks%1

.if false then begin
	The axiom

!!c1:	%2∀x s.(isblock x ⊃ ∃y.on(x,y,s))%1

and

!!c2:	%2∀x y s.(isblock x ∧ on(x,y,s) ⊃ isblock y ∨ y = Table)%1

state that every block is on something and if it isn't a block, it's
the table.
.end

	The axiom

!!c3:	%2∀x y s.(∀z.¬prevents(z,move(x,y),s) ⊃ on(x,y,result(move(x,y),s)))%1

states that unless something prevents it, ⊗x is on ⊗y in the
situation that results from the action ⊗move(x,y). 

We now list various "things" that may prevent this action.

!!c4:	%2∀x y s.(¬isblock x ∨ ¬isblock y ⊃ prevents(NONBLOCK,move(x,y),s))%1

!!c5:	%2∀x y s.(¬clear(x,s) ∨ ¬clear(y,s) ⊃ prevents(COVERED,move(x,y),s))%1

!!c6:	%2∀x y s.(tooheavy x ⊃ prevents(weight x,move(x,y),s))%1.

	Let us now suppose that a heuristic program would like to
move block ⊗A onto block ⊗C in a situation ⊗s0.  The program should
conjecture from ({eq c3}) that the action ⊗move(A,C) would have the
desired effect, so it must try to establish ⊗∀z.¬prevents(z,move(A,C),s0). 
The predicate ⊗λz.prevents(z,move(A,C),s0) 
can be circumscribed in the conjunction of
the sentences resulting from specializing 
({eq c4}), ({eq c5}) and ({eq c6}),
and this gives

.begin nofill
.turn on "→"
.skip 1
!!c7:	∂(10)%2(¬isblock A ∨ ¬isblock C ⊃ qF(NONBLOCK))
→∧_∂(10)(¬clear(A,s0) ∨ ¬clear(C,s0) ⊃ qF(COVERED))
→∧_∂(10)(tooheavy A ⊃ qF(weight A))
→∧_∂(10)∀z.(qF(z) ⊃ prevents(z,move(A,C),s0))
∂(15)⊃_∀z.(prevents(z,move(A,C),s0) ⊃ qF(z))%1
.end

which says that the only things that can prevent the move are the
phenomena described in 
({eq c4}), ({eq c5}) and ({eq c6}).  Whether ({eq c7}) is true depends on
how good the program was in finding all the relevant statements.
Since the program wants to show that nothing prevents the move, it must
set %2∀z.(qF(z) ≡ false)%1, after which ({eq c7}) simplifies to

.begin nofill
.turn on "→"
.skip 1
!!c8:	∂(10)%2(isblock A ∧ isblock B ∧ clear(A,s0) ∧ clear(B,s0) ∧ ¬tooheavy A 
∂(15)⊃ ∀z.¬prevents(z,move(A,C),s0)%1.
.end

We suppose that the premisses of this implication are to be obtained
as follows:

	1. ⊗isblock_A and ⊗isblock_B are explicitly asserted.

	2. Suppose that the only %2on%1ness assertion explicitly given
for situation ⊗s0 is
⊗on(A,B,s0).  Circumscription of ⊗λx_y.on(x,y,s0) in this assertion gives

!!c9:	%2qF(A,B) ∧ ∀x y.(qF(x,y) ⊃ on(x,y,s0)) _⊃_ ∀x y.(on(x,y,s0) ⊃ qF(x,y))%1,

and taking %2qF(x,y) ≡ x=A ∧ y=B%1 yields

!!c10:	%2∀x y.(on(x,y,s0) ⊃ x=A ∧ y=B)%1.

Using

!!c11:	%2∀x s.(clear(x,s) ≡ ∀y.¬on(y,x,s))%1

as the definition of ⊗clear yields the second two desired premisses.

	3. ⊗¬tooheavy(x) might be explicitly present or it might also
be conjectured by a circumscription assuming that if ⊗x were too heavy,
the facts would establish it.

	Circumscription may also be convenient for asserting that
when a block is moved, everything that cannot be proved to move
stays where it was.  In the simple blocks world, the effect of this
can easily be achieved by an axiom that states that all blocks except
the one that is moved stay put.  However, if there are various sentences
that say (for example) that one block is attached to another, circumscription
may express the heuristic situation better than an axiom.
.<<.bb Circumscription in the Blocks World>>
.deb←false
.if deb then begin
.skip 2
.bb Circumscription in the Blocks World

	Here is a formalization of the blocks world in which circumscription
is used to keep open the set of possible circumstances that may
prevent a block ⊗x from being moved onto a block ⊗y.  We use the
situation calculus of (McCarthy and Hayes 1969).

	A situation ⊗s is a snapshot of the world at an instant of
time.  We write ⊗on(x,y,s) to say that block ⊗x is on block ⊗y in
situation ⊗s.  %2s'_=_move(x,y,s)%1 is the new situation ⊗s' that results
the action of moving block ⊗x onto block ⊗y in situation ⊗s is attempted.
If the preconditions for the action to be successful are satisfied, we
will have %2on(x,y,s')%1.

	We begin with a static world, in which we want to use
circumscription to avoid stating more on-ness relations than
necessary.  Specifically, we would like circumscription to
give us

	1. A block is clear unless contrary evidence exists.

	2. A block is on the table unless contrary evidence exists.

	3. Only those blocks exist for which there is evidence.

	Suppose we have sentences ⊗on(A,B), ⊗on(B,C) and ⊗on(D,E), where
⊗A, ... , ⊗E are specific blocks.  We have the axiom

	%2∀x.(x ≠ Table ⊃ ∃y.on(x,y))%1

asserting that every block except the table is supported.  The
axiom schema

	%2qF(A,B) ∧ qF(B,C) ∧ qF(D,E) ⊃ ∀x y.(on(x,y) ∧ y ≠ Table ⊃ qF(x,y))%1

insures that the only ⊗on(x,y) relations are those explicitly stated except
that all blocks not mentioned as on something else are on the table.

	
	The effect of motion is given by

	%2∀x y s.(movable(x,y,s) ⊃ on(x,y,move(x,y,s))%1.

There are various known causes of immovability.  Thus
we may have

	%2∀x y z s.(on(z,x,s) ⊃ ¬movable(x,y,s))%1,

	%2∀x y z s.(on(z,y,s) ⊃ ¬movable(x,y,s))%1

and

	%2∀x y s.(tooheavy x ⊃ ¬movable(x,y,s))%1.

If these are all the causes of immovability that we wish to take into
account, we may combine the above into a single sentence

!!e1:	%2∀s x y z.(on(z,x,s) ∨ on(z,y,s) ∨ tooheavy x ⊃ ¬movable(x,y,s))%1.

The converse of ({eq e1}) may be written as a circumscription in the form

	%2∀s.[∀x y z.[on(z,x,s) ∨ on(z,y,s) ∨ tooheavy x ⊃ qF(x,y,s)] ⊃
		⊃ ∀x y.[¬movable(x,y,s) ⊃ qF(x,y,s)]]%1.

Of course, the converse can be written directly as

!!e2:  %2∀s x y z.(¬movable(x,y,s) ⊃ on(z,x,s) ∨ on(z,y,s) ∨ tooheavy x)%1.

Thus circumscription is a kind of converse and requires a schema to express it
only when the set of objects to be circumscribed is inductively defined.

CHECK OUT REMARK[E79,JMC] TO SEE IF IT SHOULD BE INCLUDED.
.end
.<<#. %3Remarks%1>>
.skip 2
#. %3Remarks and Acknowledgements%1

	1. Circumscription is not a "non-monotonic logic".
It is a form of non-monotonic reasoning augmenting ordinary first order logic.
Of course, sentence schemata are not properly handled by most present
general purpose resolution theorem provers.  Even fixed schemata of
mathematical induction when used for proving programs correct usually require
human intervention or special heuristics, while here the
program would have to use new schemata produced by circumscription.
In (McCarthy 1979b) we treat some modalities in first order logic
instead of in modal logic.  In our opinion, it is better to avoid
modifying the logic if at all possible, because there are many
temptations to modify the logic, and it would be very difficult
to keep them compatible.

	2. The default case reasoning provided in many systems is less
general than circumscription.  Suppose, for example, that
a block ⊗x is considered to be on a block ⊗y only if this is
explicitly stated, i.e. the default is that ⊗x is not on ⊗y. 
Then for each individual block ⊗x, we may be able to conclude
that it isn't on block ⊗A, but we will not be able to conclude,
as circumscription would allow, that there are no blocks on ⊗A.  That
would require a separate default statement that a block is clear
unless something is stated to be on it.

	3. The conjunct %2∀qx.(qF(qx) ⊃ P(qx))%1 in the premiss of ({eq a1})
is the result of
suggestions by Ashok Chandra (August 1979) and Patrick Hayes (September
1979) whom I thank for their help.  Without it, circumscribing a
disjunction, as in the second example in section 4, would lead to
a contradiction.

	4. The most direct way of using circumscription in AI is in a
heuristic reasoning program that represents much of what it believes by
sentences of logic.  The program would sometimes apply circumscription
to certain predicates in sentences.  In particular, when it wants to
perform an action that might be prevented by something, it circumscribes
the prevention predicate in a sentence ⊗A representing the information
being taken into account.

	Clearly the program will have to include domain dependent
heuristics for deciding what circumscriptions to make and when to
take them back.

	5. In circumscription it does no
harm to take irrelevant facts into account.  If these facts do not
contain the predicate symbol being circumscribed, they will appear
as conjuncts on the left side of the implication unchanged.  Therefore,
the original versions of these facts can be used in proving the
left side.

	6. Circumscription can be used in other formalisms than
first order logic.  Suppose for example that a set ⊗a satisfies
a formula ⊗A(a) of set theory.  The circumscription of this formula
can be taken to be

!!d1:	%2∀x.(A(x) ∧ (x ⊂ a) ⊃ (a ⊂ x))%1.

If ⊗a occurs in ⊗A(a) only in expressions of the form %2z ε a%1,
then its mathematical properties should be analogous to those of
predicate circumscription.  We have not explored what happens if
formulas like %2a_ε_z%1 occur.

	7. The results of circumscription depend on the set of predicates
used to express the facts.  For example, the same facts about
 the blocks world can be
axiomatized using the relation ⊗on or the relation ⊗above considered
in section 4 or also in terms of the heights and horizontal positions
of the blocks.  Since the results of circumscription will differ
according to which representation is chosen, we see that the
choice of representation has epistemological consequences if
circumscription is admitted as a rule of conjecture.
Choosing the set of predicates in terms of which to axiomatize as
set of facts, such as those about blocks, is like choosing a co-ordinate
system in physics or geography.  As discussed in (McCarthy 1979a),
certain concepts are definable only relative to a theory.  What theory
admits the most useful kinds of circumscription may be an important
criterion in the choice of predicates.  It may also be possible to
make some statements about a domain like the blocks world
in a form that does not depend on the language used.

	8. This investigation
was supported in part by ARPA Contract MDA-903-76-C-0206,
ARPA Order No. 2494,
in part by NSF Grant MCS 78-00524, in part by the IBM 1979 Distinguished Faculty
Program at the T. J. Watson Research Center, and in part by the Center
for Advanced Study in the Behavioral Sciences.
.<<NOTES ON POSSIBLE INCLUSIONS>>
.if deb then begin
.at "qpi" ⊂"%2p%4i%2"⊃
.at "qpj" ⊂"%2p%4j%2"⊃


1. Maybe we can consider propositional and domain circumscription as instances
of a common concept if we allow ourselves to introduce an arbitrary
partial ordering of models of sets of sentences and consider minimal
models with respect to this ordering.  We probably want to restrict the
ordering so that there will be some syntactic counterpart of minimal
inference.  Actually propositional circumscription doesn't meet this
requirement without modification, but anyway it's desirable.
THIS CONSIDERATION IS OBSOLETED BY PREDICATE CIRCUMSCRIPTION.

2. Perhaps the right way to reduce propositional circumscription to
domain circumscription is to replace each propositional variable
%2p%4i%1 by the wff %2∃x.(index x = i)%1.  In that way minimizing
the truth of the proposition is accomplished by minimizing the existence
of the %2x%1's.  The purpose of %2index x = i%1 is to make sure that the
existence of the %2x%1's can be minimized separately.  We need to be
sure that no other object has an integer index, but we can introduce
axioms that require them all to have the non-integer JUNK as index.
ALSO OBSOLETE

This raises the problem of whether there is an analogous way of
treating predicates %2p(u,v)%1.  Maybe we want to replace it by
%2∃x.(p'(u,v,x)_∧_index_x_=_i)%1 or perhaps instead of %2_=_i%1, we
should have %2_=_<u,v,i>%1.

3. CIRCUM[1,CLT] is the following example:

Consider the following problem (told to CLT by DrewMcD, ascribed to Bmoore):

You are told that the only things on the table are things that you can prove
are on the table.  Further you are told that A is on the table and B is on 
the table and that there is something red on the table.   You would like to
be able to conclude that either A is red or B is red.

Circumscription can be applied to solve this problem.   We formalize the 
problem in a language L=<<Ontable,Red>,<>,<A,B>> where Ontable and Red 
are unary.  The theory is:

	(1) Ontable(A)
	(2) Ontable(B)
	(3) ∃x.(Ontable(x)∧Red(x))

Circumscribing with respect to (1) and (2) we obtain the schema:

	(4) qF(A)∧qF(B) ⊃ ∀x.qF(x)

and it is easy to jump to the conclusion that 

	(5) ∀x.(x=A∨x=B)

and thus to conclude that Red(A)∨Red(B).

Notice that if the circumscription is done with respect to  all three facts
then we lose.  Namely we get the schema

	(6) qF(A)∧qF(B)∧∃x.(qF(x)∧Ontable(x)∧Red(x)) ⊃ ∀x.qF(x)

then we only conclude

	(7) ∀x.(x=A∨x=B∨Red(x))

which does not allow us to show that either A or B is red.

4. The essence of the Moore-McDermott example is included in the
following simpler example.

	There is one constant A and one sentence ∃x.Red(x).  Circumscribing
on the constant only gives qF(A) ⊃ ∀x.qF(x) and specializing qF
by ∀x.(qF(x) ≡ x = A) establishes ∀x.(x = A) from which  Red(A) follows.
Circumscribing on both A and ∃x.Red(x) gives

	qF(A) ∧ ∃x.(qF(x) ∧ Red(x)) ⊃ ∀x.qF(x)

from which it doesn't look like we can infer Red(A).

	It looks like circumscription doesn't give us what is true
in all minimal models but only what is true in all minimal models
contained in arbitrary models, i.e. a sentence p  is provable by
circumscribing a set of sentences A iff every model M of A
is such that every minimal model M' of A contained in M satisfies p.
THE ABOVE WAS A MISTAKE.  At least in the above case the model
with two objects - A and a red one - is indeed minimal w/r
α{A , ∃x.Red(x)α}.

5. Imitation semantics.  Suppose we replace some of the predicate symbols
of a theory by a new symbols with one more argument - a world.  Thus
Red(x) is replaced by Red(x,w).  Some of the properties of model theory
can now be axiomatized within the theory.  The process can be repeated by
adding another "outer" world parameter, but we shall discuss only a single
such "semanticization" to begin with.

	Every term and wff now depends on w - assuming, as we shall for now,
that we apply each predicate to the same variable w as we build up the
wffs.  We can quantify over w, so that ∀w.<wff> will enjoy some of the
properties of validity and ∃w.<wff> will have some of the properties of
satisfiability.

	How to axiomatize w is not immediately obvious.  One idea is to
imagine a common domain of non-w s and introduce a predicate
exists(x,w).  (I confess a weakness for theories in which something
like existence is a predicate).  This allows a definition of ordering
.begin nofill

	%2w1 < w2 ≡ ∀x.(exists(x,w1) ⊃ exists(x,w2)) 
∧ ∀xy.(exists(x,w1) ∧ exists(y,w1) ⊃ (P(x,y,w1) ≡ P(x,y,w2)) 
∧ ...%1

.end

where ... indicates that there is a wff similar to that on the second line
for each predicate in the language.
This will permit us to define minimal worlds.

	Our ability to imitate real model theory will depend on our tools
for asserting the existence of enough worlds.  If the domain is infinite
and there is even one unary predicate symbol, the number of interpretations
is already non-denumerable, and the L%C:%*owenheim-Skolem theorem already tells
us that no axiomatization can insure that.

	A certain amount can be done by postulating that for every world
w there is a world w' that gives the same value to all predicates except
that a single predicate has a single value changed.  We can also imagine
other changes whose possibility can be stated.  The main purpose of such
axiomatizations will be to insure that certain formulas or at least enough
formulas are "satisfiable".

	"Completeness" can also be defined as asserting that all "valid"
formulas are provable.

	I think all this is related to circumscription, but I can't now
make the connection.

6. Propositional circumscription can be done by introducing worlds as
follows:

	Each propositional variable %2p%4i%1 is replaced by a function
%2qpi(w)%1.

	We write

	%2w1 ≤ w2 ≡ ∀i.[qpi(w1) ⊃ qpi(w2)]%1

where we may suppose that the quantification over ⊗i actually designates
a conjunction over the set of propositional variables to be circumscribed.

	Minimality is defined by

	%2minimal w ≡ ∀w1.(w1 ≤ w ⊃ w1 = w)%1.

	A wff in the original formulation becomes a %2wff(w)%1 in the
new.  We write %2wff1_qe_wff2%1 if

	%2∀w.(wff1(w) ∧ minimal w ⊃ wff2(w))%1.

5. Further note on propositional circumscription

	Perhaps the right analog of the qF of domain circumscription
is to replace a formula by another that contains a free propositional
parameter - call it π.  Circumscribing sets this parameter to whatever
value is convenient.  Thus suppose we have

	%2leakyboat ⊃ cantgo%1,

and we either do or don't have the additional formula %2leakyboat%1.
The circumscription formula should then be either

	%2leaky ∧ (leaky ⊃ π) ⊃ (π ⊃ cantgo)%1

or just

!!j1:	%2(leaky ⊃ π) ⊃ (π ⊃ cantgo)%1.

In the former case, taking π to be false leads to a tautology, since the
left side of the main implication is false.  In the second case it
leads to the converse

	%2¬leakyboat ⊃ ¬cantgo%1

which is a step in the right direction anyway.
Where ({eq j1}) is to come from is still not clear.

6. Chandra wants to weaken circumscription, because circumscribing ⊗R in
%2R(a) ∨ R(b)%1 leads to

!!j2:	%2qF(a) ∨ qF(b) ⊃ ∀x.(R(x) ⊃ qF(x))%1,

and if %2a ≠ b%1, taking %2qF(x)%1 to be successively %2x = a%1 and %2x = b%1
leads to a contradiction.  He suggests

!!j3:	%2A(qF) ⊃ ∀x.(R(x) ⊃ qF(x)) ∨ [∃x.(R(x)∧¬qF(x)) ∧ ∃x.(¬R(x)∧qF(x))]%1,

from which we would like to get %2¬R(c)%1 by circumscribing %2R(a)∨R(b)%1.

*****

	Assume ∃c.(c≠a ∧ c≠b ∧ R(c)).  We have the cases

%2R(a) ∧ R(c),  qF(x) ≡ x=a%1

%2R(b) ∧ R(c),  qF(x) ≡ x=b%1

We will have ¬(2) ∧ ¬(3).

	Chandra suggests that ⊗R is a minimal relation rather than
the minimal relation.  There's a bit more, but it's unintelligible.
.end
.<<addendum>>
.skip 2
.cb "ADDENDUM: CIRCUMSCRIPTION AND OTHER NON-MONOTONIC FORMALISMS"

	Circumscription and
the non-monotonic reasoning
formalisms of McDermott and Doyle (1980) and Reiter (1980) differ along
two dimensions.  First, circumscription is concerned with minimal
models, and they are concerned with arbitrary models.
It appears that these approaches solve somewhat different though
overlapping classes of problems, and each has its uses.  The other
difference is that the reasoning of both other formalisms
involves models directly, while the syntactic formulation of
circumscription uses axiom schemata.  Consequently, their systems
are incompletely formal unless the metamathematics is also formalized.
and this hasn't yet been done.

	However, schemata are applicable to other formalisms
than circumscription.  Suppose, for example, that we have some axioms about
trains and their presence on tracks, and we wish to express the fact
that if a train may be present, it is unsafe to cross the tracks.
In the McDermott-Doyle formalism, this might be expressed

!!f1:	%2M on(train,tracks) ⊃ ¬safe-to-cross(tracks)%1,

where the properties of the predicate %2on%1 are supposed
expressed in a formula that we
may call %2Axiom(on)%1.  The %2M%1 in ({eq f1}) stands for "is
possible".
We propose to replace ({eq f1}) and %2Axiom(on)%1 by
the schema

!!f2:	%2Axiom(qF) ∧ qF(train,tracks) ⊃ ¬safe-to-cross(tracks)%1,

where qF is a predicate parameter that can be replaced by any
predicate expression that can be written in the language being
used.  If we can find a qF that makes the left hand side of
({eq f2}) provable, then we can be sure that %2Axiom(on)%1
together with %2on(train,tracks)%1 has a model assuming that
%2Axiom(on)%1 is consistent.  Therefore, the schema ({eq f2})
is essentially a consequence of the McDermott-Doyle formula
({eq f1}).  The converse isn't true.  A predicate symbol may have
a model without there being an explicit formula realizing it.
I believe, however, that the schema is usable in all cases
where the McDermott-Doyle or Reiter formalisms can be practically
applied, and, in particular, to all the examples in their papers.

	(If one wants a counter-example to the usability of the schema,
one might look at the membership relation  of set theory with
the finitely axiomatized
Goedel-Bernays set theory as the axiom.  Instantiating qF in this case
would amount to giving an internal model of set theory, and
this is possible only in a stronger theory).

	It appears that such use of schemata amounts
to importing part of the model theory of a subject into the
theory itself.  It looks useful and even essential for common
sense reasoning, but its logical properties are not obvious.

	We can also go frankly to second order logic and write

!!f3:	%2∃qF.(Axiom(qF) ∧ on(train,tracks) ⊃ ¬safe-to-cross(tracks))%1.

Second order reasoning, which might be in set theory or a formalism
admitting concepts as objects rather than in second order logic,
seems to have the advantage that some of the predicate and function
symbols may be left fixed and others imitated by predicate parameters.
This allows us to say something like, "For any interpretation of
⊗P and ⊗Q satisfying the axiom ⊗A, if there is an interpretation in
which ⊗R and ⊗S satisfy the additional axiom ⊗A', then it is unsafe
to cross the tracks".  This maybe needed to express common sense
non-monotonic reasoning and it seems more powerful than any of
the above-mentioned non-monotonic formalisms including circumscription.

	The train example is a non-normal default in Reiter's sense,
because we cannot conclude that the train is on the tracks
in the absence of evidence to the contrary.  Indeed, suppose that we want to
wait for and catch a train at a station across the tracks.  If there might
be a train coming we will take a bridge rather than a shortcut across
the tracks, but we don't want to jump to the conclusion that there is a train,
because then we would think we were too late and give up trying to catch it.
The statement can be reformulated as a normal default by writing

!!f4:	%2M ¬safe-to-cross(tracks) ⊃ ¬safe-to-cross(tracks)%1,

but this is unlikely to be equivalent in all cases and the non-normal
expression seems to express better the common sense facts.

	Like normal defaults, circumscription doesn't deal with
possibility directly, and a circumscriptive treatment of the train
problem would involve circumscribing %2safe-to-cross(tracks)%1 in
the set of axioms.  It therefore might not be completely satisfactory.

.skip 2
.<<#. %3References%1>>
.skip 2
#. %3References%1

%3Amarel, Saul (1971)%1: "On Representation of Problems of Reasoning
about Actions", in D. Michie (ed.), %2Machine Intelligence 3%1,
Edinburgh University Press, pp. 131-171.

%3Chandra, Ashok (1979)%1: personal conversation, August.

%3Davis, Martin (1980)%1: "Notes on the Mathematics of Non-Monotonic
Reasoning", %2Artificial Intelligence%1, this issue.

%3Hayes, Patrick (1979)%1: personal conversation, September.

%3Hewitt, Carl (1972)%1: %2Description and Theoretical Analysis
(Using Schemata) of PLANNER: a Language for Proving Theorems and
Manipulating Models in a Robot%1, MIT AI Laboratory TR-258.

%3McCarthy, John (1960)%1: "Programs with Common Sense", %2Proceedings of
the Teddington Conference on the Mechanization of Thought Processes%1, H.M.
Stationery Office, 1960.

%3McCarthy, John (1960)%1: "Programs with Common Sense", %2Proceedings of
the Teddington Conference on the Mechanization of Thought Processes%1, H.M.
Stationery Office, 1960.

%3McCarthy, John and Patrick Hayes (1969)%1:  "Some Philosophical
Problems from the Standpoint of Artificial Intelligence," 
in D. Michie (ed), %2Machine Intelligence 4%1, American Elsevier, New York, NY.

%3McCarthy, John (1977)%1:
"Epistemological Problems of Artificial Intelligence", %2Proceedings
of the Fifth International Joint Conference on Artificial 
Intelligence%1, M.I.T., Cambridge, MA.

%3McCarthy, John (1979a)%1:
"Ascribing Mental Qualities to Machines", %2Philosophical Perspectives 
in Artificial Intelligence%1, Martin Ringle, ed., Harvester Press, July 1979.

%3McCarthy, John (1979b)%1: 
"First Order Theories of Individual Concepts and Propositions", 
in Michie, Donald (ed.) %2Machine Intelligence 9%1,
University of Edinburgh Press.

%3McDermott, Drew and Jon Doyle (1980): "Non-Monotonic Logic I",
%2Artificial Intelligence%1, this issue.

%3Reiter, Raymond (1980)%1: "A Logic for Default Reasoning",
%2Artificial Intelligence%1, this issue.

%3Sussman, G.J., T. Winograd, and E. Charniak (1971)%1:
%2Micro-Planner Reference Manual, AI Memo 203%1, M.I.T. AI Lab.

This version of CIRCUM.W80[S79,JMC] PUBbed at {time} on {date}.